k:, f, g:(k), p:(k).
sum(if p(i) f(i)+g(i) else f(i) fi | i < k)
=
sum(f(i) | i < k)+sum(if p(i) g(i) else 0 fi | i < k) 

latex

Definitions	t  T, x:A. B(x), x(s), if b t else f fi, {i..j}, primrec(n;b;c), AB, P & Q, i  j < k, P  Q, False, A, b, b, Prop, , P  Q, Unit, i=j, S  T, S  T, , sum(f(x) | x < k), ij
Lemmas	ge wf, nat properties, nat wf, int seg wf, not functionality wrt iff, assert of eq int, eq int wf, bool wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, le wf, primrec wf, ifthenelse wf